\section{From RTL to ABA}

Let $\phi$ be a PSL formula over $P$ in \emph{negation normal form} (NNF), i.e., negation operators only occur in front of propositions. We define the 2ABA $\autA$ that is language-equivalent to $\phi$. Let $\autA_\alpha, \autA'_\alpha, \autB_\alpha, \autB'_\alpha$, be the NFAs and NBAs for a semi-extended regular expression $\alpha \in Sub(\phi)$ as defined in the paper. We define $\autA := (Q, \delta, \phi, F)$ over $P$ as follows. 


\begin{itemize}
	\item $Q := \set{\qI} \cup Sub(\phi) \cup Q_3$, where $Q_3$ is defined in the paper.
	\item The transition function\footnote{The definition of the fixpoints deviate from the definition in our paper. However, this definition produces less states. To get the definition of the paper, we just have to adapt the definition of $\delta(\psi_1 \lor \psi_2)$} is defined as $\delta(q)$ is the first component of $\delta'(q)$, where $\delta': \calB^+(Q) \to \calB^+(P' \cup (Q \times \bbD')) \times \set{-1,0,1,2}$ is defined as follows.
		\begin{itemize}
			\item $\delta'(p) := (p, 0)$,\quad for $p \in P$
			\item $\delta'(\neg p) := (\neg p, 0)$,\quad for $p \in P$
			\medskip

			\item $\delta'(\psi_1 \land \psi_2) := 
				(\psi'_1 \land \psi'_2, a \otimes b)$
			
			\item $\delta'(\psi_1 \lor \psi_2) := 
				\begin{cases}
					(\tup{\psi_1, 0} \lor \psi'_2, b) & \text{if } a \otimes b = 2 \\
					(\psi'_1 \lor \psi'_2, a \otimes b) & \text{otherwise }
				\end{cases}$
			\medskip
			
			\item $\delta'(X\psi_1) := (\tup{\psi_1, 1}, 1)$
			\item $\delta'(Y\psi_1) := (\tup{\psi_1, -1}, -1)$
			\item $\delta'(Z\psi_1) := (\tup{\psi_1, \opZ}, -1)$
			\medskip
			
			\item $\delta'(\psi_1 U \psi_2) := \delta'(\psi_2 \lor (\psi_1 \land X(\psi_1 U \psi_2)))$
			\item $\delta'(\psi_1 R \psi_2) := \delta'(\psi_2 \land (\psi_1 \lor X(\psi_1 U \psi_2)))$
			\item $\delta'(\psi_1 S \psi_2) := \delta'(\psi_2 \lor (\psi_1 \land Y(\psi_1 U \psi_2)))$
			\item $\delta'(\psi_1 T \psi_2) := \delta'(\psi_2 \land (\psi_1 \lor Z(\psi_1 U \psi_2)))$
			\medskip
			
			\item $\delta'(s, \alpha \fby \psi) := 
					\delta'(\bigvee_{(g, t) \in \eta(s)} (g \land (f(t,\psi) \lor \opX(t,\alpha \fby \psi))))$,\\
					where $f(q,\psi) := \opX\psi$ if $q \in E$, and $\false$, otherwise.

			\item $\delta(s, \alpha \bfby \psi) :=$ as above with $\opY$ instead of $\opX$.
			\medskip
			
			\item $\delta'(s, \alpha \trig \psi) := 
					\delta'(\bigwedge_{(g, t) \in \eta(s)} (g \to (f(t,\psi) \land \opX(t,\alpha \fby \psi))))$,\\
					where $f(q, \psi) := \opX\psi$ if $q \in E$, and $\true$, otherwise.
			
			\item $\delta(s, \alpha \btrig \psi) :=$ as above with $\opZ$ instead of $\opX$.

			\item \dots
		\end{itemize}
		where we use the abbreviations $\delta'(\psi_1) =: (\psi'_1, a)$, $\delta'(\psi_2) =: (\psi'_2, b)$, and
		\[
			a \otimes b := 
			\begin{cases}
				0 & \text{if } (a,b) = (0,0) \\
				-1 & \text{if } (a,b) \in \set{(0,-1),(-1,0),(-1,-1)} \\
				1 & \text{if } (a,b) \in \set{(0,1),(1,0),(1,1)} \\
				2 & \text{otherwise.}
			\end{cases}
		\]
		Note that $\delta'$ is overloaded for $\lor$ and $\land$.
	\item $F$ is defined as in the paper.	
\end{itemize}

It is straightforward to transform $\autA$ into a locally 1-way ABA. We just replace every tuple of the form $(q, -1)$ and $(q, \opZ)$ by $(Yq, 0)$ and $(Zq, 0)$, respectively.